Step of Proof: decidable__assert
9,38
postcript
pdf
Inference at
*
I
of proof for Lemma
decidable
assert
:
b
:
. Dec(
b
)
latex
by ((((Unfold `decidable` 0)
CollapseTHEN (D 0))
)
CollapseTHENA ((Auto_aux (first_nat 1:n
C
) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term)))
latex
C
1
:
C1:
1.
b
:
C1:
(
b
)
(
(
b
))
C
.
Definitions
t
T
,
Dec(
P
)
,
x
:
A
.
B
(
x
)
Lemmas
bool
wf
origin